A:Type, l:IdLnk, tg:Id, ds:x:Id fp Type, conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
(k:Knd. (k  dom(conds))  (hasloc(k;source(l))))
 (triggersGlue(A; l; tg; ds; conds)  Realizer) 

latex

Definitions

Type, t  T, IdLnk, Id, x. t(x), x:A. B(x), a:A fp B(a), Knd, Top, left + right, x:AB(x), State(ds), x:A  B(x), x.A(x), source(l), hasloc(k;i), b, KindDeq, x  dom(f), P  Q, triggersGlue(A; l; tg; ds; conds), Realizer, Atom$n, if b then t else f fi , f(x), trigger-send(A;ds;x;cond;l;tg), fpf-domain(f), map(f;as), type List, xL.R(x), (x  l), {x:A| B(x)} , [car / cdr], [], Rsframe(lnk;tag;L), (L), s = t, a < b, P  Q, P & Q, P  Q, #$n, ||as||, Void, False, A, A  B, , , l[i], A c B, EqDecider(T), , FinProbSpace, DeclaredType(ds;x), , Unit, rec(x.A(x)), mapl(f;l)

Lemmas

mapl wf, unit wf, rationals wf, decl-type wf, finite-prob-space wf, bool wf, l member wf, length wf nat, nat wf, select wf, trigger-send wf, fpf-ap wf, member-fpf-dom, es realizer wf, Rsframe wf, fpf-domain wf, Rlist wf, fpf-dom wf, Kind-deq wf, assert wf, hasloc wf, lsrc wf, fpf-trivial-subtype-top, decl-state wf, top wf, Knd wf, fpf wf, Id wf, IdLnk wf